the_w:World, l:IdLnk, i:Id, a:Action(i). isrcv(l;a)   

latex

Definitions	x:A. B(x), t  T, isrcv(l;a), p  q, b, P  Q, tt, if b then t else f fi , ff, , , Unit, P  Q, P & Q,
Lemmas	w-isnull wf, bool wf, eqtt to assert, bfalse wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, isrcv wf, w-kind wf, eq lnk wf, lnk wf, w-action wf, Id wf, IdLnk wf, world wf